|
|
Invariants of jet groups and applications in continuum mechanics
Buriánek, Martin ; Doupovec, Miroslav (referee) ; Kureš, Miroslav (advisor)
This thesis is focused on jet groups and their matrix representations. The opening section deals with group representations, group actions on sets and invariants of actions. Another section explains terms such as smooth manifolds, Lie group and Lie algebra. The following part clarifies terms jet and jet group as a special example of Lie group. First of all, groups $G_1^r$ and $G_n^1$ are described, then description of group $G_n^2$ and its subgroups ensues. Representations of these jet groups are proposed. Finally, applications of jet groups in continuum mechanics are mentioned. The thesis is complemented with algorithm of chosen problems in program Wolfram Mathematica.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout způsob vedoucí ke zvýšení přesnosti analýzy programů pomocí nástroje 2LS, založený na existujících konceptech, a to hlavně na syntézi invariant na základě šablon. 2LS je nástroj pro statickou analýzu programů napsaných v jazyce C, který využívá SMT solver a abstraktní interpretaci k automatickému odvození invariant. V případě kdy 2LS nedokáže rozhodnout zda je program správný, navrhované řešení analyzuje invarianty vypočítané v různých abstraktních doménách, a identifikuje takové části invariant, které mohou s největší pravděpodobností způsobit nejednoznačnost verifikace. Pomocí těchto získaných informací, dokáže navrhnutá metoda identifikovat proměnné původního programu, na kterých pravděpodobně závisí úspěch verifikace. Výstup tohoto řešení může posloužit jako zpětná vazba indikující proměnné, jejíchž problematické hodnoty by měly být omezeny. Také může být výstup využit vývojáři 2LS pro účely debugování při vývoji nových analýz. Řešení bylo implementováno v nástroji 2LS. Na základě různých experimentů mezinárodní soutěže ve verifikaci programů SV-COMP, dokáže řešení identifikovat proměnné způsobující nejednoznačnost verifikace ve více než polovině programů, na kterých verifikace momentálně selhává.
|
|
|
The use of invariants of geometric transformations to solving problems
Doubrava, Jiří ; Zamboj, Michal (advisor) ; Beran, Filip (referee)
This thesis deals with the division of bijective collinear geometric mappings. It deals with a corresponding view on its respective problems and their solutions. The main part of the thesis is a collection of solved problems in the field of plane geometry, which are divided into several groups. The thesis can be used by both mathematics teachers and students at the secondary schools. The thesis is divided into two parts; the first part is theoretical and it contains a brief introduction to the basic concepts concerning invariants of geometric transformations and a description of the structure of geometry according to Felix Klein including his Erlangen program; the second part contains the actual assignments and so- lutions of the problems. The solutions of some of the problems are supplemented by im- ages created in GeoGebra software for better illustration. The images play an important role even in the theoretical part, where they can help improve understanding of some of the more complex concepts. Some of the problems were created by the author, other prob- lems are taken from sources listed in the list of bibliography. KEYWORDS geometric transformations, groups, Erlangen program, invariant, solved problems
|
|
|
Invariants of jet groups and applications in continuum mechanics
Buriánek, Martin ; Doupovec, Miroslav (referee) ; Kureš, Miroslav (advisor)
This thesis is focused on jet groups and their matrix representations. The opening section deals with group representations, group actions on sets and invariants of actions. Another section explains terms such as smooth manifolds, Lie group and Lie algebra. The following part clarifies terms jet and jet group as a special example of Lie group. First of all, groups $G_1^r$ and $G_n^1$ are described, then description of group $G_n^2$ and its subgroups ensues. Representations of these jet groups are proposed. Finally, applications of jet groups in continuum mechanics are mentioned. The thesis is complemented with algorithm of chosen problems in program Wolfram Mathematica.
|
|
|
Improving Precision of Program Analysis in the 2LS Framework
Smutný, Martin ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout způsob vedoucí ke zvýšení přesnosti analýzy programů pomocí nástroje 2LS, založený na existujících konceptech, a to hlavně na syntézi invariant na základě šablon. 2LS je nástroj pro statickou analýzu programů napsaných v jazyce C, který využívá SMT solver a abstraktní interpretaci k automatickému odvození invariant. V případě kdy 2LS nedokáže rozhodnout zda je program správný, navrhované řešení analyzuje invarianty vypočítané v různých abstraktních doménách, a identifikuje takové části invariant, které mohou s největší pravděpodobností způsobit nejednoznačnost verifikace. Pomocí těchto získaných informací, dokáže navrhnutá metoda identifikovat proměnné původního programu, na kterých pravděpodobně závisí úspěch verifikace. Výstup tohoto řešení může posloužit jako zpětná vazba indikující proměnné, jejíchž problematické hodnoty by měly být omezeny. Také může být výstup využit vývojáři 2LS pro účely debugování při vývoji nových analýz. Řešení bylo implementováno v nástroji 2LS. Na základě různých experimentů mezinárodní soutěže ve verifikaci programů SV-COMP, dokáže řešení identifikovat proměnné způsobující nejednoznačnost verifikace ve více než polovině programů, na kterých verifikace momentálně selhává.
|
|
|
Plato´s Vision of the Ideal State and Dystopias in the 20th century
LACUŠKOVÁ, Petra
In this thesis I will deal with the comparison of Plato´s vision of the ideal state presented in his work Constitution to negative utopias in the 20th century. I will seek common invariants occuring in all presented works by using method of structural analysis formulated by Claude Lévi-Strauss. The subjects of my analysis are books Constitution, We, Brave New World, 1984 and movies Metropolis, Matrix and Equilibrium. In the end I will present my hypothesis that there is another invariant fact that all negative utopias are based on raising the economic character of a man in order to maximize effect of his work. This is done by suppression and destruction of John Dewey´s concept of an experience.
|
guest ::
